| 1: | terms(N) | → cons(recip(sqr(N)),terms(s(N))) | |
| 2: | sqr(0) | → 0 | |
| 3: | sqr(s(X)) | → s(add(sqr(X),dbl(X))) | |
| 4: | dbl(0) | → 0 | |
| 5: | dbl(s(X)) | → s(s(dbl(X))) | |
| 6: | add(0,X) | → X | |
| 7: | add(s(X),Y) | → s(add(X,Y)) | |
| 8: | first(0,X) | → nil | |
| 9: | first(s(X),cons(Y,Z)) | → cons(Y,first(X,Z)) | |
| 10: | half(0) | → 0 | |
| 11: | half(s(0)) | → 0 | |
| 12: | half(s(s(X))) | → s(half(X)) | |
| 13: | half(dbl(X)) | → X | |
| 14: | TERMS(N) | → SQR(N) | |
| 15: | TERMS(N) | → TERMS(s(N)) | |
| 16: | SQR(s(X)) | → ADD(sqr(X),dbl(X)) | |
| 17: | SQR(s(X)) | → SQR(X) | |
| 18: | SQR(s(X)) | → DBL(X) | |
| 19: | DBL(s(X)) | → DBL(X) | |
| 20: | ADD(s(X),Y) | → ADD(X,Y) | |
| 21: | FIRST(s(X),cons(Y,Z)) | → FIRST(X,Z) | |
| 22: | HALF(s(s(X))) | → HALF(X) | |